c formula generated with seed 1, probabilty values 0.414000 0.028000 0.503000 and clause ration 4.408571
c the planted solution is {1, 8, 9, 10, 13, 15, 16, 17, 18, 19, 22, 27, 28, 30, 31, 32, 33, 36, 38, 40, 41, 43, 46, 47, 49, 50, 55, 56, 57, 58, 61, 66, 71, 73, 78, 82, 84, 85, 89, 91, 94, 95, 96, 97, 98, 104, 109, 111, 112, 113, 115, 117, 124, 125, 127, 133, 134, 135, 137, 138, 139, 140, 141, 146, 147, 150, 151, 152, 153, 154, 155, 159, 162, 163, 166, 167, 169, 170, 171, 173, 175, 178, 179, 180, 181, 182, 184, 185, 186, 191, 192, 195, 196, 201, 202, 205, 207, 210, 211, 215, 216, 217, 218, 220, 222, 224, 225, 226, 227, 228, 233, 235, 238, 239, 242, 243, 244, 246, 247, 248, 249, 250, 251, 253, 254, 256, 258, 259, 260, 262, 263, 266, 268, 272, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 290, 291, 292, 294, 295, 297, 298, 299, 300, 303, 308, 311, 312, 313, 316, 317, 318, 322, 323, 324, 329, 330, 333, 334, 336, 337, 338, 347, 348, 349}
p cnf 350 1543
-124 -287 -24 0
-112 -209 -109 0
-62 205 -145 0
129 -215 -296 0
-279 285 164 0
245 163 -15 0
-6 -88 -289 0
227 -208 292 0
250 254 -26 0
38 -217 310 0
-137 -101 158 0
75 24 256 0
-110 -132 71 0
-88 -231 27 0
-166 78 89 0
333 -235 245 0
-151 -143 339 0
124 304 -15 0
-120 -350 -296 0
-338 -99 -138 0
-223 -302 185 0
-135 232 300 0
-53 231 -141 0
81 306 238 0
176 -80 -243 0
306 -99 -1 0
-236 -27 -281 0
113 -246 274 0
-348 282 269 0
-196 78 289 0
-123 -259 -28 0
258 312 -183 0
6 -349 18 0
180 -58 121 0
-301 -213 217 0
126 251 -17 0
23 -160 187 0
-53 -247 120 0
34 25 169 0
-98 72 -2 0
65 50 116 0
63 331 49 0
3 22 -233 0
-121 -151 -97 0
114 -188 310 0
128 -1 -208 0
-303 -195 272 0
-346 -349 293 0
143 325 243 0
-310 -286 -19 0
-338 326 171 0
222 333 -339 0
112 -53 17 0
-178 213 -83 0
20 290 315 0
216 164 122 0
-45 180 -203 0
43 -318 319 0
-98 -12 -280 0
-281 -30 -339 0
-297 331 278 0
20 71 -36 0
-287 -93 149 0
-64 313 278 0
329 -241 186 0
-160 151 -79 0
135 -344 96 0
-224 -214 -47 0
-113 10 25 0
192 272 -257 0
215 20 -246 0
298 229 203 0
331 -107 345 0
-159 241 -81 0
313 -40 -247 0
344 94 69 0
280 1 303 0
-28 235 -224 0
160 -55 111 0
-121 140 180 0
-78 322 310 0
322 -342 -160 0
216 -184 108 0
159 129 -282 0
58 38 -100 0
52 -285 -64 0
-124 43 204 0
281 -43 54 0
-239 311 269 0
108 -338 333 0
17 231 48 0
-74 235 163 0
-55 281 -61 0
275 101 -116 0
332 -21 -85 0
166 112 258 0
147 -317 252 0
-119 -132 173 0
82 314 187 0
-209 307 128 0
-45 316 313 0
55 201 1 0
185 15 -176 0
134 334 -39 0
28 128 251 0
284 -173 160 0
-20 -297 -56 0
43 -22 130 0
-43 -102 -139 0
121 90 -39 0
333 -77 254 0
233 16 -265 0
-278 237 -34 0
313 312 222 0
-279 -291 298 0
-25 -336 28 0
-246 276 171 0
-196 -170 182 0
-107 232 -299 0
90 179 -89 0
-345 95 -305 0
130 150 203 0
317 -44 -42 0
-168 -44 139 0
216 33 -157 0
301 -69 345 0
-151 -149 -74 0
-33 26 313 0
287 -149 -53 0
246 54 270 0
-46 182 236 0
-77 -310 -63 0
-301 326 -89 0
235 209 -323 0
5 -207 32 0
114 -68 62 0
79 -76 42 0
193 -175 -48 0
19 -125 245 0
-14 -122 277 0
-38 -15 -79 0
-242 -229 -228 0
-189 148 -127 0
189 -177 -242 0
182 106 -28 0
223 3 196 0
258 114 200 0
-350 -6 -116 0
47 186 147 0
-249 -331 161 0
-213 181 -335 0
110 167 276 0
225 54 -16 0
-213 329 -229 0
-39 -105 -343 0
-19 -329 47 0
-260 2 -198 0
-332 302 320 0
16 -83 33 0
-140 117 -338 0
270 -67 -281 0
349 -121 -241 0
136 -42 -104 0
-45 -265 -114 0
-108 -250 -272 0
13 330 -23 0
102 17 -298 0
-146 298 -279 0
211 -95 51 0
55 127 -252 0
-323 103 -128 0
107 -62 -135 0
-340 -195 92 0
-241 218 -125 0
-138 -191 330 0
68 -60 193 0
26 -121 -260 0
338 314 -22 0
123 -160 310 0
29 167 -127 0
41 225 -51 0
-336 -203 -349 0
179 -301 -157 0
-86 28 263 0
-19 125 -49 0
-161 289 155 0
-204 123 -207 0
173 102 -348 0
-190 -8 -166 0
20 284 -317 0
-325 -231 -237 0
46 -171 -162 0
-276 -54 -129 0
-265 41 133 0
-226 230 -265 0
206 142 -92 0
-288 302 -159 0
-88 -238 321 0
-350 222 15 0
132 8 -111 0
-162 -242 -4 0
-259 177 -241 0
-143 94 -315 0
90 -342 -18 0
76 -342 -210 0
-83 315 -298 0
-226 -302 172 0
-47 129 -121 0
12 -234 -290 0
68 295 200 0
172 -180 226 0
291 -168 -12 0
-49 88 224 0
163 56 -274 0
-195 125 -141 0
-152 -137 -232 0
-108 -248 -134 0
-309 -350 -80 0
127 -348 -183 0
-243 -70 -278 0
147 -21 85 0
334 -23 -344 0
51 333 60 0
1 -274 -265 0
44 324 -272 0
155 40 -231 0
-315 -41 221 0
-232 -116 70 0
-266 -347 -23 0
-127 318 289 0
-227 50 120 0
11 -111 -119 0
-313 100 -25 0
-184 -312 -93 0
256 70 2 0
228 153 207 0
-66 314 235 0
72 285 -282 0
-212 16 28 0
117 -88 -194 0
-206 -21 25 0
-212 -265 33 0
181 -185 -207 0
-28 72 202 0
-331 55 326 0
206 295 -195 0
-233 -34 -186 0
-88 129 -175 0
-222 339 -271 0
131 -3 -250 0
-345 -23 152 0
269 -106 53 0
-183 -150 158 0
-283 121 175 0
112 216 -52 0
216 -291 -290 0
79 -169 -23 0
-30 86 -110 0
147 -112 -220 0
-30 190 191 0
-138 -268 -187 0
346 58 33 0
-100 205 348 0
228 -198 -76 0
-201 -148 212 0
254 301 56 0
119 -262 -92 0
296 -247 249 0
247 109 135 0
23 284 132 0
334 234 -28 0
-237 -312 -248 0
-182 -76 148 0
204 -257 239 0
-333 -287 58 0
-164 -200 -300 0
-92 -202 -84 0
-343 -240 82 0
239 162 -319 0
-100 -312 -43 0
-307 11 6 0
237 26 268 0
-265 344 -278 0
108 -148 14 0
-144 27 43 0
94 -42 -209 0
-69 333 151 0
324 -285 -287 0
-228 -259 -183 0
-330 129 96 0
176 -17 -305 0
-347 -203 -16 0
-54 329 -88 0
-287 137 -31 0
-241 158 293 0
167 -5 292 0
307 68 -203 0
-218 95 -249 0
148 155 -308 0
-331 176 -178 0
-304 -237 -130 0
-272 188 -172 0
301 -40 -107 0
-275 -211 -201 0
-52 253 -177 0
-105 -166 -96 0
-281 245 -302 0
36 90 203 0
-278 287 328 0
-307 258 91 0
198 333 -281 0
126 -346 -139 0
78 -247 -242 0
174 -124 78 0
62 102 -176 0
210 -326 153 0
159 42 3 0
72 -178 272 0
18 66 -183 0
-174 137 -4 0
42 247 264 0
156 -337 242 0
-326 -70 294 0
26 311 60 0
-283 134 -209 0
242 -96 -323 0
-231 12 -169 0
244 -39 -123 0
-103 29 245 0
-174 -270 -76 0
168 268 122 0
-261 -248 345 0
-301 -274 106 0
2 -279 287 0
194 -308 247 0
1 215 -51 0
-194 -243 93 0
-115 -273 -94 0
-293 325 -50 0
17 -108 -44 0
-306 290 -257 0
-124 31 131 0
33 -285 72 0
95 -97 11 0
95 209 -141 0
103 -273 -294 0
78 176 -227 0
-34 42 -18 0
-261 -307 -53 0
-299 10 -244 0
-125 41 -66 0
-285 -250 153 0
-4 -235 -333 0
248 153 -255 0
-80 283 -325 0
55 306 -89 0
-104 -301 -202 0
-265 220 298 0
-307 -27 138 0
291 -210 167 0
-335 281 -326 0
-293 210 97 0
158 32 223 0
-239 212 -69 0
-182 -186 -35 0
-293 -317 -28 0
-199 -328 182 0
246 -324 219 0
-223 264 -249 0
148 -48 -113 0
115 -140 230 0
253 -197 -79 0
-81 -329 105 0
2 270 170 0
147 -331 -189 0
-305 245 -56 0
114 208 -306 0
139 347 312 0
12 289 -208 0
64 -343 165 0
195 322 207 0
-127 203 -26 0
-129 208 346 0
94 -7 222 0
194 217 87 0
225 191 96 0
-152 -88 -169 0
-264 -92 -213 0
171 -31 -202 0
-75 172 200 0
-93 291 297 0
-245 2 -224 0
-255 -32 86 0
-127 190 228 0
313 244 192 0
-21 143 -117 0
150 -303 -137 0
3 68 290 0
-148 -59 196 0
96 -263 102 0
-259 348 296 0
87 -142 221 0
36 -44 -74 0
8 3 -317 0
-87 42 -73 0
274 -257 -268 0
330 98 134 0
201 -91 157 0
-260 243 101 0
62 -190 -96 0
-131 180 323 0
32 341 -259 0
-150 338 7 0
-160 -81 299 0
-85 -58 -23 0
208 130 138 0
165 266 -210 0
-123 -125 114 0
-64 -104 321 0
232 -219 265 0
-82 -70 -336 0
151 3 223 0
202 304 62 0
15 137 19 0
85 -9 282 0
251 -83 291 0
267 -246 169 0
-72 329 -240 0
301 -223 188 0
-212 165 198 0
-56 309 -148 0
-64 -4 61 0
-316 -76 -169 0
73 187 -71 0
43 -128 210 0
22 -80 -164 0
-192 -241 6 0
-151 -63 116 0
-52 28 -143 0
85 90 76 0
330 -197 -223 0
16 271 -269 0
-92 81 -169 0
49 261 -297 0
250 -244 335 0
65 206 -271 0
69 309 222 0
-160 326 -94 0
77 -178 -328 0
-84 -341 236 0
-142 -24 196 0
-253 315 284 0
-64 132 -140 0
200 -148 -262 0
296 -277 192 0
283 282 -307 0
313 -198 -99 0
-167 313 176 0
206 -238 284 0
64 166 -58 0
-300 47 54 0
140 -330 142 0
40 29 132 0
102 227 -247 0
164 102 -293 0
171 -63 79 0
-77 -3 24 0
-62 161 -184 0
42 26 167 0
-129 52 -159 0
226 271 -146 0
-51 -102 111 0
52 -205 1 0
335 -1 215 0
-302 44 -263 0
168 236 -332 0
285 172 -180 0
-17 -144 -40 0
-305 20 -235 0
85 282 -289 0
-80 -48 -45 0
346 -58 -350 0
57 -217 -18 0
-315 151 27 0
228 -267 281 0
295 -23 318 0
-170 -191 205 0
-247 296 -76 0
-154 -315 -340 0
-282 112 136 0
175 78 291 0
238 -154 -91 0
-232 315 -18 0
286 193 -323 0
-274 -9 71 0
88 114 -331 0
-146 -261 -213 0
-306 -240 -130 0
-6 325 129 0
268 -295 276 0
7 268 156 0
-317 114 -34 0
-82 -303 192 0
-188 66 155 0
183 -184 33 0
-122 -22 -215 0
315 238 26 0
35 -79 315 0
-280 -249 -60 0
39 11 169 0
143 144 -214 0
152 33 337 0
-85 -279 61 0
172 -176 321 0
-319 165 -38 0
275 -161 -233 0
-336 -80 52 0
-218 -281 -75 0
-273 264 -47 0
-172 340 -117 0
-252 212 -166 0
-91 -36 -271 0
334 -157 216 0
302 252 -74 0
-251 -225 -307 0
60 122 205 0
65 195 -43 0
-47 -188 122 0
-183 -236 117 0
125 -76 -83 0
165 -220 -304 0
-310 25 -256 0
34 328 -108 0
30 -268 200 0
112 -88 243 0
320 276 171 0
-254 229 135 0
-95 256 42 0
-25 85 135 0
-280 -15 73 0
-190 60 149 0
215 165 -155 0
-226 -91 -319 0
218 135 -144 0
285 261 176 0
-269 -24 -90 0
-19 172 235 0
204 8 -66 0
-188 -301 242 0
74 -58 180 0
119 -298 159 0
-245 -96 -97 0
-229 -2 -296 0
-36 -232 305 0
-120 45 -299 0
-178 -106 -202 0
-106 -82 -256 0
342 -168 -313 0
224 308 -164 0
134 -252 258 0
295 283 -344 0
-121 -142 140 0
292 97 -319 0
79 -253 16 0
147 -149 337 0
236 52 311 0
-186 -148 21 0
-165 -170 114 0
-199 -171 188 0
280 -61 -78 0
-62 335 -297 0
-182 237 334 0
328 -155 152 0
249 -178 267 0
75 334 -242 0
129 -198 -337 0
299 -304 -270 0
276 -328 -295 0
349 147 -39 0
133 114 161 0
115 -77 57 0
-11 239 -100 0
-315 298 -240 0
281 47 -53 0
-144 311 -221 0
72 -219 213 0
-125 307 -187 0
-188 -147 231 0
-348 217 -292 0
323 -264 -92 0
151 -175 -329 0
322 -205 144 0
-102 81 -207 0
228 -197 218 0
-332 -333 123 0
-3 -259 99 0
132 336 203 0
192 225 318 0
-209 336 -80 0
192 -67 -231 0
251 -76 253 0
213 -300 -101 0
-34 -281 -243 0
-163 -31 -63 0
22 301 331 0
-55 271 78 0
-301 117 -103 0
-40 -70 -307 0
235 30 -317 0
296 69 -119 0
-317 222 -227 0
137 343 -40 0
60 -315 -56 0
-318 112 177 0
110 -329 -145 0
338 -282 -13 0
-169 49 229 0
253 118 174 0
-225 8 -170 0
-223 284 288 0
-144 -30 51 0
-269 -336 119 0
217 165 199 0
302 30 -242 0
227 272 82 0
28 -198 117 0
-346 112 -44 0
272 140 127 0
-289 -230 262 0
222 -229 -65 0
-211 319 167 0
-107 -252 111 0
94 -131 -235 0
-339 258 47 0
28 92 219 0
-204 -327 155 0
-112 -337 330 0
-47 195 -9 0
203 -310 174 0
-125 241 146 0
-272 -212 245 0
-50 -105 -205 0
44 -247 -92 0
247 -315 291 0
239 -336 131 0
-182 174 31 0
89 37 -347 0
-53 228 225 0
269 -27 295 0
287 -256 51 0
-85 -306 -217 0
248 236 122 0
-145 337 -172 0
87 -3 -82 0
261 13 -97 0
63 -25 120 0
-62 -123 73 0
-203 84 -306 0
-250 -80 267 0
257 93 -198 0
-21 -257 -160 0
-83 96 313 0
41 254 -172 0
-290 212 1 0
-283 -224 85 0
274 171 -253 0
281 -129 -275 0
-136 -195 79 0
-296 -283 158 0
350 -132 -266 0
203 -257 -322 0
-235 -265 -104 0
-268 79 -214 0
-281 261 71 0
-71 214 242 0
-205 -122 177 0
156 -130 -290 0
209 194 -70 0
136 -18 -221 0
39 -253 -237 0
344 -283 180 0
227 158 -266 0
324 90 77 0
-40 -109 -240 0
125 -147 7 0
215 251 -144 0
-305 -29 40 0
-345 324 -237 0
-210 181 -180 0
-9 11 134 0
-299 -79 186 0
24 311 209 0
216 27 191 0
230 273 140 0
253 117 -271 0
3 285 131 0
-259 203 224 0
21 -338 -237 0
-260 230 -232 0
184 -54 98 0
244 303 -37 0
36 -350 -34 0
-1 348 -260 0
-219 134 -264 0
-163 320 -223 0
-275 -101 216 0
176 108 -188 0
-265 -7 181 0
217 262 -20 0
-293 -344 -168 0
-7 -3 111 0
-4 235 -11 0
245 156 330 0
80 -185 -107 0
100 63 166 0
-1 -157 -32 0
322 -330 -329 0
-240 -89 14 0
-65 43 -255 0
53 -21 -275 0
-73 342 -193 0
270 51 348 0
-276 109 247 0
-24 215 133 0
81 -17 -93 0
312 120 174 0
-259 313 -173 0
67 -250 277 0
-229 162 -161 0
-6 -326 -264 0
-231 -84 -225 0
62 70 18 0
310 134 51 0
-97 -38 -69 0
-256 188 163 0
-190 6 -233 0
-166 -269 -10 0
-8 -344 149 0
-264 -28 -134 0
-85 -315 346 0
-43 -259 139 0
59 69 -99 0
323 56 151 0
-259 184 -300 0
-95 -132 106 0
-123 -21 283 0
-298 -229 274 0
144 -276 174 0
-137 -306 219 0
244 3 219 0
-261 174 304 0
246 279 -74 0
-272 -228 -108 0
87 260 319 0
-349 -336 -344 0
145 342 -39 0
-350 -17 -153 0
-303 -264 188 0
-339 216 -307 0
163 38 -344 0
-174 120 -159 0
107 -313 -343 0
321 -4 -43 0
296 226 83 0
313 -62 170 0
-173 164 -145 0
337 299 -219 0
98 -6 256 0
-277 -191 41 0
-234 287 61 0
123 -189 255 0
7 -280 47 0
-292 119 -203 0
90 -48 -224 0
124 17 239 0
179 82 -332 0
226 194 234 0
-116 -278 -113 0
-45 -139 14 0
-309 -321 -177 0
89 276 293 0
-297 247 26 0
-1 317 -334 0
160 300 -295 0
41 -114 91 0
77 -84 -116 0
-8 -338 -174 0
230 299 106 0
-302 94 -134 0
91 -345 272 0
-20 -36 -3 0
162 47 -106 0
-40 -3 -8 0
-292 -145 257 0
-237 -337 -133 0
291 -89 72 0
-207 175 -192 0
134 311 -90 0
-121 80 -233 0
-93 291 169 0
-246 40 83 0
279 -210 -249 0
-33 -61 -144 0
90 102 196 0
-332 26 -43 0
-25 194 213 0
-64 32 -293 0
-121 -91 309 0
-326 -141 -66 0
-200 -128 -53 0
311 150 -243 0
48 -140 -118 0
-14 279 -274 0
-91 -177 -16 0
-168 30 153 0
288 -95 262 0
235 17 175 0
190 -107 -215 0
-125 278 42 0
2 -116 -205 0
213 -296 23 0
-109 175 -211 0
49 176 -211 0
-188 -94 -150 0
-168 -123 236 0
-227 -42 -342 0
-332 -102 -11 0
-25 144 245 0
-199 29 254 0
221 244 9 0
199 200 311 0
-25 -33 -159 0
-184 325 32 0
57 202 -174 0
-167 -47 -121 0
103 -301 -10 0
258 -280 52 0
-350 26 -104 0
-273 284 -276 0
71 -77 -64 0
-286 -42 -58 0
300 295 -234 0
-271 -126 1 0
277 336 -158 0
-326 -236 31 0
104 18 215 0
169 211 -346 0
101 -286 170 0
-176 3 346 0
91 -192 168 0
-6 61 196 0
-128 -35 57 0
-328 165 190 0
155 215 -306 0
206 244 -32 0
-288 -163 21 0
-280 91 236 0
-269 142 232 0
166 9 182 0
246 138 47 0
-79 -166 -258 0
-312 8 -33 0
187 -315 -173 0
122 260 102 0
8 -44 28 0
-174 55 -208 0
-332 174 267 0
135 -148 210 0
-125 208 -110 0
48 79 17 0
-295 20 -206 0
-54 -158 170 0
46 -204 -274 0
-76 -173 42 0
-317 350 224 0
-107 -90 74 0
-124 275 -345 0
-277 -150 -346 0
324 -202 118 0
139 258 140 0
-197 167 -149 0
-188 -168 -88 0
126 -204 267 0
235 -245 -320 0
-109 -178 186 0
194 318 77 0
320 342 -102 0
-38 263 -169 0
70 283 -243 0
312 -128 -223 0
95 319 59 0
-348 111 -250 0
176 -78 -101 0
-20 318 186 0
-38 77 -304 0
-43 192 189 0
136 178 4 0
-306 -207 -311 0
-229 -344 -204 0
-86 63 -141 0
-175 277 -217 0
-278 -285 -344 0
-149 70 -251 0
271 314 292 0
265 133 -58 0
24 43 105 0
-248 242 51 0
110 109 114 0
190 156 -168 0
-15 229 272 0
-251 170 209 0
-303 -245 -210 0
91 -205 325 0
-170 196 -195 0
317 -191 4 0
84 -29 -273 0
-69 276 -150 0
-57 219 -271 0
45 -319 53 0
-307 156 -272 0
93 78 3 0
-284 -295 163 0
292 -294 168 0
-179 -47 17 0
260 169 322 0
-79 231 -297 0
196 59 -135 0
-244 58 -1 0
258 -306 292 0
311 173 207 0
-35 130 63 0
-220 -244 -214 0
-336 -153 -221 0
91 286 236 0
-56 -46 -42 0
38 75 342 0
205 -263 -227 0
-297 -265 -210 0
-90 -71 245 0
207 278 196 0
300 -201 -184 0
258 268 92 0
181 -192 62 0
-230 237 14 0
314 -120 -237 0
-348 -45 174 0
-5 -131 49 0
-99 -36 213 0
-80 334 22 0
119 -184 58 0
208 -85 333 0
-260 -119 4 0
-225 -286 -65 0
323 162 294 0
324 -336 70 0
-218 322 -36 0
-19 -158 -303 0
244 -49 -58 0
213 164 -209 0
73 327 67 0
-263 42 -144 0
252 260 -56 0
-273 89 316 0
113 196 -59 0
-144 -109 252 0
248 -84 208 0
214 34 317 0
-259 -220 -231 0
-234 68 -134 0
-307 274 -337 0
-133 341 251 0
-300 -5 126 0
-177 172 -146 0
215 -78 342 0
281 -210 121 0
55 -30 -324 0
-321 -167 76 0
-242 -9 322 0
-251 -177 -155 0
183 -338 349 0
301 -22 -92 0
241 318 12 0
68 -244 -126 0
-109 66 -98 0
-275 -46 -115 0
85 -46 -303 0
-349 -178 -130 0
266 -237 -29 0
93 289 163 0
-350 -131 323 0
261 -129 -27 0
5 -135 13 0
-155 -188 16 0
-194 210 16 0
96 -309 -126 0
-100 -24 147 0
-106 -154 -173 0
-41 292 -58 0
-72 176 -170 0
283 41 -259 0
-189 -156 -68 0
61 196 -62 0
339 89 -94 0
-105 -178 92 0
-135 -106 144 0
54 292 155 0
276 263 110 0
122 -143 105 0
-203 -153 -180 0
-56 211 118 0
322 284 155 0
-180 -257 116 0
-110 -184 252 0
314 46 148 0
-59 -190 84 0
203 -60 98 0
-293 -99 -11 0
141 197 -134 0
211 304 -112 0
-184 179 -55 0
-49 -69 193 0
285 229 -251 0
-213 111 -128 0
122 224 267 0
291 218 -77 0
-221 309 321 0
319 -79 212 0
137 -121 -88 0
-63 -100 97 0
-174 273 -10 0
250 58 -4 0
3 -240 -287 0
201 99 -155 0
-265 217 -105 0
243 248 -257 0
-316 344 282 0
211 4 -192 0
-208 14 149 0
169 64 -8 0
-49 229 -319 0
-273 -125 241 0
206 267 -198 0
221 214 170 0
-297 -282 -64 0
65 -4 67 0
-197 -254 110 0
131 -203 -263 0
292 10 197 0
158 -343 289 0
-283 -261 -184 0
-21 5 320 0
334 -225 -167 0
-186 -74 -205 0
184 -167 -180 0
339 274 -231 0
-325 253 76 0
294 50 -34 0
211 -151 -49 0
-199 -338 -159 0
5 -174 -202 0
-14 348 -257 0
142 -4 315 0
-45 328 -238 0
215 235 -257 0
116 157 -70 0
-45 55 57 0
-313 261 109 0
-95 180 148 0
223 101 324 0
-301 50 -76 0
296 -151 -88 0
-220 -32 -346 0
-91 300 132 0
147 -59 336 0
181 159 -160 0
81 -244 -83 0
-34 300 -265 0
-67 237 -246 0
-294 -84 155 0
125 -334 340 0
4 -222 323 0
168 -98 294 0
-290 12 -320 0
293 -99 345 0
219 -11 90 0
18 -162 35 0
-174 4 -248 0
-139 297 -287 0
-294 -316 -172 0
-181 -19 -54 0
154 187 -10 0
2 66 -261 0
-21 175 84 0
-274 -191 -179 0
-6 -240 -89 0
-163 257 153 0
-289 159 225 0
41 -108 -144 0
-114 195 90 0
240 242 -338 0
-259 -219 -111 0
-272 -349 -288 0
337 -118 -288 0
-134 202 236 0
-65 -19 331 0
-154 313 -50 0
274 76 235 0
181 340 77 0
80 329 126 0
-282 -291 134 0
-289 -51 185 0
323 -225 -250 0
77 161 -116 0
48 159 193 0
-68 -143 147 0
-82 144 -136 0
280 190 305 0
96 -77 137 0
-3 210 265 0
-312 130 -301 0
19 162 -301 0
87 -161 -191 0
-131 -98 143 0
188 183 222 0
-63 113 228 0
-323 -246 318 0
-15 -148 189 0
-113 299 168 0
226 -244 64 0
315 -281 -310 0
-153 -129 -254 0
-37 88 275 0
158 122 -315 0
-35 204 -268 0
249 -22 331 0
-327 96 259 0
259 -333 -55 0
-24 -80 -305 0
-331 -98 122 0
164 104 208 0
-283 145 235 0
315 -73 266 0
-128 -274 251 0
-3 272 -307 0
-43 55 340 0
-331 71 -271 0
-33 169 -55 0
271 -137 277 0
-245 -74 -149 0
211 254 -232 0
-32 -328 12 0
-246 111 -109 0
5 49 63 0
-4 289 14 0
79 107 57 0
-174 -25 -6 0
-217 41 70 0
208 -64 188 0
142 -203 -215 0
-235 -108 213 0
-105 -164 268 0
85 253 138 0
135 77 350 0
-23 171 -74 0
-338 -210 30 0
193 -39 -338 0
288 124 54 0
-255 78 298 0
-245 111 239 0
-86 219 -151 0
31 -202 -246 0
60 2 -275 0
28 -312 -343 0
232 258 -281 0
-111 64 -77 0
-227 329 234 0
173 175 -231 0
-307 182 -121 0
-42 -72 9 0
-167 127 -115 0
-144 244 -221 0
-323 -343 345 0
-182 -76 -317 0
208 -254 -120 0
-140 -9 -197 0
119 -237 -347 0
-82 -10 -26 0
-44 293 121 0
-330 -155 280 0
-119 -68 -114 0
-137 -53 -251 0
112 -244 145 0
-320 -163 -227 0
-275 78 -37 0
285 -282 98 0
-234 -280 69 0
-298 -34 83 0
3 -44 70 0
-142 -114 -183 0
245 105 227 0
152 41 -209 0
-178 -222 -275 0
-206 332 -49 0
322 210 -288 0
87 -253 -275 0
48 -209 -41 0
176 -91 -42 0
-234 -270 226 0
250 40 280 0
-200 107 -328 0
-106 145 -43 0
-29 166 -83 0
-156 125 -14 0
147 -6 -90 0
-113 -74 -50 0
273 -331 51 0
-157 198 -316 0
-40 210 120 0
-63 80 198 0
-111 166 -290 0
-96 -77 118 0
196 -50 -56 0
304 134 165 0
314 -123 257 0
-166 167 161 0
201 -274 -220 0
-101 199 143 0
127 142 265 0
268 89 336 0
-267 -159 346 0
283 -211 -185 0
-88 331 53 0
278 -274 170 0
197 -176 -242 0
-273 271 231 0
-196 324 255 0
13 -75 336 0
37 -258 15 0
-265 -269 -72 0
47 -349 136 0
-138 130 249 0
-27 341 153 0
-23 -225 -162 0
236 -282 -68 0
-281 268 -154 0
291 21 -210 0
-92 -340 205 0
-136 74 -311 0
-97 -150 -106 0
184 -137 -292 0
38 -241 61 0
195 -134 -323 0
-295 -278 -219 0
89 -67 162 0
-243 -267 245 0
-145 -310 -326 0
-60 332 -267 0
213 252 -53 0
216 174 257 0
-309 -349 -224 0
334 -200 333 0
86 -187 105 0
-285 -225 -342 0
47 -320 17 0
-285 -59 -242 0
-202 -150 -252 0
125 -160 -198 0
110 266 234 0
-209 177 219 0
-91 -276 341 0
183 81 227 0
43 -311 112 0
-141 28 -182 0
-117 -215 -62 0
318 272 -261 0
-137 -247 -203 0
20 -136 -133 0
-264 308 -64 0
-133 -145 72 0
-66 -198 -292 0
-161 -318 79 0
316 -150 -244 0
132 -331 -13 0
-287 -309 341 0
-317 187 -183 0
-274 -54 292 0
206 -96 -136 0
-32 119 -213 0
343 300 -140 0
-125 -210 -267 0
328 -47 159 0
-261 -322 25 0
126 114 272 0
73 -174 -144 0
243 220 122 0
278 283 -321 0
-70 321 -97 0
-184 -80 -311 0
247 333 97 0
150 243 -129 0
61 -95 -169 0
137 39 -78 0
89 -326 -148 0
-63 223 48 0
-274 244 54 0
14 242 11 0
282 66 247 0
-297 202 350 0
-8 175 80 0
-13 29 250 0
178 -117 -239 0
209 -324 334 0
-289 -14 -39 0
96 -154 76 0
-8 25 -241 0
-118 81 -19 0
-151 218 -249 0
-89 348 -169 0
131 -197 341 0
-214 41 -76 0
-281 182 314 0
-146 -98 -296 0
235 150 -326 0
-269 348 -12 0
334 -213 283 0
77 -104 -212 0
-157 -121 -328 0
130 -192 -269 0
277 216 -90 0
-272 -20 198 0
227 -171 -262 0
-270 154 205 0
-29 -313 -225 0
-228 139 251 0
178 -110 -90 0
-59 -83 113 0
-25 165 34 0
-256 -79 -294 0
77 129 294 0
347 57 -122 0
-151 310 167 0
-314 90 -253 0
279 347 247 0
297 273 176 0
54 11 -289 0
276 -183 -280 0
-4 317 -187 0
-174 11 -15 0
212 5 55 0
283 217 71 0
-290 -154 94 0
219 -312 9 0
209 341 244 0
-166 130 -325 0
6 -124 -264 0
122 -319 304 0
271 164 -307 0
216 -220 -55 0
345 58 301 0
-125 347 68 0
-74 81 -336 0
219 -297 248 0
116 301 -21 0
-76 266 247 0
-212 -184 128 0
-299 184 -134 0
-305 275 -78 0
213 99 -183 0
-332 -38 188 0
126 335 140 0
284 -350 330 0
-325 -246 7 0
-73 -229 100 0
-309 348 -229 0
-264 218 -65 0
284 -276 58 0
-341 -118 -136 0
-304 331 -226 0
6 -302 -27 0
-319 104 -230 0
6 -268 -304 0
179 -239 100 0
-82 183 210 0
321 -136 63 0
18 313 227 0
-92 263 40 0
277 -244 234 0
-349 298 275 0
-66 27 339 0
49 -135 -228 0
-320 -164 -289 0
-121 -38 -155 0
69 44 311 0
-207 -266 127 0
6 -350 168 0
-301 -218 -235 0
117 266 36 0
-304 -198 -346 0
66 -21 151 0
-155 75 225 0
203 40 241 0
274 -343 -141 0
45 52 -339 0
-340 94 110 0
-7 244 -142 0
-118 249 338 0
-77 -253 156 0
111 -114 96 0
-156 -262 52 0
-119 -184 138 0
155 253 279 0
-129 -87 181 0
-26 -348 -18 0
-343 -206 17 0
-85 -204 -146 0
126 269 -157 0
-99 219 -318 0
35 -343 224 0
-112 -304 343 0
230 -211 -45 0
322 -294 -18 0
-62 -260 189 0
-147 -88 108 0
-282 79 196 0
-307 339 -239 0
184 147 -132 0
-283 290 -10 0
-15 182 -184 0
-256 113 310 0
-320 281 41 0
-94 34 -328 0
231 -248 -69 0
-159 332 -114 0
173 -328 278 0
218 -93 -3 0
-289 187 156 0
39 170 -258 0
-320 216 -102 0
208 -241 123 0
305 212 27 0
57 -226 79 0
117 16 -75 0
289 -195 104 0
-35 -231 89 0
-120 237 -348 0
155 159 141 0
-151 -152 -204 0
216 350 -38 0
253 -7 279 0
-126 -315 -289 0
-199 243 -309 0
-110 195 -106 0
-346 -211 -251 0
273 -306 -222 0
25 136 220 0
-93 -155 -202 0
339 -26 270 0
-4 206 -220 0
267 -237 -294 0
-192 155 -178 0
348 153 192 0
-259 94 -66 0
-198 -55 7 0
344 194 -174 0
2 25 311 0
-246 128 225 0
-248 323 204 0
114 144 -261 0
-169 -114 42 0
-53 122 -97 0
-292 -32 -340 0
112 -199 130 0
202 166 -271 0
70 291 346 0
250 135 -35 0
338 50 -81 0
-218 205 -268 0
202 178 -143 0
-148 -336 64 0
-87 251 146 0
-168 -201 -166 0
-124 -21 -266 0
299 -312 143 0
258 -234 307 0
-184 183 -142 0
-22 136 196 0
65 -250 41 0
-56 40 -152 0
235 134 -271 0
-227 -244 262 0
-258 266 -43 0
-42 -85 3 0
332 113 123 0
320 60 85 0
196 -153 -154 0
193 -28 -189 0
-12 92 -186 0
175 311 194 0
67 191 149 0
-206 -165 175 0
-56 111 37 0
289 116 162 0
320 342 -273 0
321 128 -172 0
140 -302 222 0
-96 52 -341 0
202 204 -117 0
307 -245 309 0
-238 235 85 0
196 59 -286 0
175 -215 -282 0
-314 -12 -78 0
57 -17 128 0
118 -175 337 0
-253 32 138 0
131 73 -49 0
220 -254 -262 0
329 258 -301 0
157 -31 347 0
310 -132 -134 0
-69 -124 -169 0
-68 84 -101 0
-346 -227 203 0
182 -122 169 0
-323 310 336 0
-186 313 59 0
270 38 114 0
74 215 -224 0
-98 91 -22 0
-147 -124 -245 0
-247 -248 -126 0
184 319 -249 0
-220 -25 327 0
287 -73 92 0
-188 -205 -152 0
71 82 104 0
-24 126 250 0
27 -161 308 0
-218 171 177 0
-186 -204 6 0
-125 101 -208 0
-217 204 285 0
280 -217 158 0